perm filename PROOFS[F80,JMC] blob
sn#554811 filedate 1981-01-05 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00002 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 <LISP>LISP.SAV133
C00053 ENDMK
C⊗;
<LISP>LISP.SAV;133
<BOYER>CODE.;1
<BOYER>CODE1.;781
<BOYER>DATA.;1
<BOYER>DATA1.;2
Thursday, November 20, 1980 4:11PM-PST!
←DEFN(NTH (U N)
(IF (ZEROP N)
U
(IF (EQUAL N 1)
(CAR U)
(NTH (CDR U) (SUB1 N)))))
The lemma SUB1.LESSP informs us that (COUNT N)
decreases according to the well-founded function LESSP in
each recursive call. Hence, NTH is accepted under the
definitional principle.
[3739 cns / 13.3 s + 0.0 gc + .6 io (= 16 @ 1)]
NTH
!
←DEFN(INDEX (U X)
(IF (NLISTP U)
0
(IF (EQUAL (CAR U) X)
1
(ADD1 (INDEX (CDR U) X)))))
The lemma CDR.LESSP can be used to prove that
(COUNT U) decreases according to the well-founded function
LESSP in each recursive call. Hence, INDEX is accepted
under the definitional principle. Observe that
(NUMBERP (INDEX U X)) is a theorem.
[1767 cns / 6.4 s + 0.0 gc + .7 io (= 9 @ 1)]
INDEX
!
←DEFN(MEMB (X Y)
(IF (NLISTP Y)
(FALSE)
(IF (EQUAL X (CAR Y))
T
(MEMB X (CDR Y)))))
The lemma CDR.LESSP informs us that (COUNT Y) goes
down according to the well-founded function LESSP in each
recursive call. Hence, MEMB is accepted under the
definitional principle. Note that:
(OR (FALSEP (MEMB X Y))
(TRUEP (MEMB X Y)))
is a theorem.
[1715 cns / 6.3 s + 0.0 gc + .6 io (= 7 @ 1)]
MEMB
!
←PROVE.LEMMA(FOO (REWRITE)
(IMPLIES (MEMB X U)
(EQUAL (NTH U (INDEX U X)) X)))
This conjecture can be simplified, using the abbreviation
IMPLIES, to:
(IMPLIES (MEMB X U)
(EQUAL (NTH U (INDEX U X)) X)),
which we will name *1.
We will appeal to induction. Two inductions are
suggested by terms in the conjecture. However, they merge
into one likely candidate induction. We will induct
according to the following scheme:
(AND (IMPLIES (NOT (LISTP U)) (p U X))
(IMPLIES (AND (LISTP U) (p (CDR U) X))
(p U X))).
The inequality CDR.LESSP establishes that the measure
(COUNT U) decreases according to the well-founded function
LESSP in the induction step of the scheme. The above
induction scheme produces the following three new
conjectures:
Case 3. (IMPLIES (AND (NOT (LISTP U)) (MEMB X U))
(EQUAL (NTH U (INDEX U X)) X)).
This simplifies, expanding the definitions of NLISTP,
INDEX, EQUAL, NTH, and MEMB, to:
T.
Case 2. (IMPLIES (AND (LISTP U)
(NOT (MEMB X (CDR U)))
(MEMB X U))
(EQUAL (NTH U (INDEX U X)) X)),
which we simplify, unfolding NLISTP, INDEX, and MEMB, to:
(IMPLIES (AND (LISTP U)
(NOT (MEMB X (CDR U)))
(EQUAL (CAR U) X))
(EQUAL (NTH U 1) X)).
However this simplifies again, expanding NUMBERP, EQUAL,
and NTH, to:
T.
Case 1. (IMPLIES (AND (LISTP U)
(EQUAL (NTH (CDR U) (INDEX (CDR U) X))
X)
(MEMB X U))
(EQUAL (NTH U (INDEX U X)) X)),
which simplifies, expanding the definitions of NLISTP,
INDEX, and MEMB, to two new formulas:
Case 1.2.
(IMPLIES
(AND (LISTP U)
(EQUAL (NTH (CDR U) (INDEX (CDR U) X))
X)
(MEMB X (CDR U))
(NOT (EQUAL (CAR U) X)))
(EQUAL (NTH U (ADD1 (INDEX (CDR U) X)))
X)),
which we again simplify, applying SUB1.ADD1 and
ADD1.EQUAL, and opening up the definitions of NUMBERP
and NTH, to:
(IMPLIES (AND (LISTP U)
(EQUAL (CDR U) X)
(MEMB X (CDR U))
(NOT (EQUAL (CAR U) X)))
(NOT (EQUAL (INDEX (CDR U) X) 0))),
which we again simplify, clearly, to:
(IMPLIES
(AND (LISTP U)
(MEMB (CDR U) (CDR U))
(NOT (EQUAL (CAR U) (CDR U))))
(NOT (EQUAL (INDEX (CDR U) (CDR U)) 0))).
Appealing to the lemma CAR/CDR.ELIM, we now replace U
by (CONS V Z) to eliminate (CDR U) and (CAR U). The
result is:
(IMPLIES (AND (MEMB Z Z) (NOT (EQUAL V Z)))
(NOT (EQUAL (INDEX Z Z) 0))).
Name the above subgoal *1.1.
Case 1.1.
(IMPLIES
(AND (LISTP U)
(EQUAL (NTH (CDR U) (INDEX (CDR U) X))
X)
(EQUAL (CAR U) X))
(EQUAL (NTH U 1) X)),
which we again simplify, opening up NUMBERP, EQUAL, and
NTH, to:
T.
So we now return to:
(IMPLIES (AND (MEMB Z Z) (NOT (EQUAL V Z)))
(NOT (EQUAL (INDEX Z Z) 0))),
which we named *1.1 above. Let us appeal to the induction
principle. There are two plausible inductions. However,
they merge into one likely candidate induction. We will
induct according to the following scheme:
(AND (IMPLIES (NOT (LISTP Z)) (p Z V))
(IMPLIES (AND (LISTP Z) (p (CDR Z) V))
(p Z V))).
The inequality CDR.LESSP establishes that the measure
(COUNT Z) decreases according to the well-founded function
LESSP in the induction step of the scheme. The above
induction scheme generates four new goals:
Case 4. (IMPLIES (AND (NOT (LISTP Z))
(MEMB Z Z)
(NOT (EQUAL V Z)))
(NOT (EQUAL (INDEX Z Z) 0))),
which we simplify, expanding the definitions of NLISTP,
INDEX, EQUAL, and MEMB, to:
T.
Case 3. (IMPLIES (AND (LISTP Z)
(NOT (MEMB (CDR Z) (CDR Z)))
(MEMB Z Z)
(NOT (EQUAL V Z)))
(NOT (EQUAL (INDEX Z Z) 0))).
This simplifies, expanding NLISTP, INDEX, and MEMB, to
two new goals:
Case 3.2.
(IMPLIES
(AND (LISTP Z)
(NOT (MEMB (CDR Z) (CDR Z)))
(MEMB Z (CDR Z))
(NOT (EQUAL V Z))
(NOT (EQUAL (CAR Z) Z)))
(NOT (EQUAL (ADD1 (INDEX (CDR Z) Z)) 0))),
which we again simplify, using linear arithmetic, to:
T.
Case 3.1.
(IMPLIES (AND (LISTP Z)
(NOT (MEMB (CDR Z) (CDR Z)))
(NOT (EQUAL V Z))
(EQUAL (CAR Z) Z))
(NOT (EQUAL 1 0))).
However this again simplifies, using linear arithmetic,
to:
T.
Case 2. (IMPLIES (AND (LISTP Z)
(EQUAL V (CDR Z))
(MEMB Z Z)
(NOT (EQUAL V Z)))
(NOT (EQUAL (INDEX Z Z) 0))),
which we simplify, unfolding NLISTP, INDEX, and MEMB, to
two new conjectures:
Case 2.2.
(IMPLIES
(AND (LISTP Z)
(MEMB Z (CDR Z))
(NOT (EQUAL (CDR Z) Z))
(NOT (EQUAL (CAR Z) Z)))
(NOT (EQUAL (ADD1 (INDEX (CDR Z) Z)) 0))).
However this again simplifies, using linear arithmetic,
to:
T.
Case 2.1.
(IMPLIES (AND (LISTP Z)
(NOT (EQUAL (CDR Z) Z))
(EQUAL (CAR Z) Z))
(NOT (EQUAL 1 0))),
which we again simplify, using linear arithmetic, to:
T.
Case 1. (IMPLIES
(AND (LISTP Z)
(NOT (EQUAL (INDEX (CDR Z) (CDR Z)) 0))
(MEMB Z Z)
(NOT (EQUAL V Z)))
(NOT (EQUAL (INDEX Z Z) 0))).
This simplifies, unfolding the definitions of NLISTP,
INDEX, and MEMB, to the following two new formulas:
Case 1.2.
(IMPLIES
(AND (LISTP Z)
(NOT (EQUAL (INDEX (CDR Z) (CDR Z)) 0))
(MEMB Z (CDR Z))
(NOT (EQUAL V Z))
(NOT (EQUAL (CAR Z) Z)))
(NOT (EQUAL (ADD1 (INDEX (CDR Z) Z)) 0))).
This simplifies again, using linear arithmetic, to:
T.
Case 1.1.
(IMPLIES
(AND (LISTP Z)
(NOT (EQUAL (INDEX (CDR Z) (CDR Z)) 0))
(NOT (EQUAL V Z))
(EQUAL (CAR Z) Z))
(NOT (EQUAL 1 0))).
However this simplifies again, using linear arithmetic,
to:
T.
That finishes the proof of *1.1, which also finishes
the proof of *1. Q.E.D.
[11248 cns / 61.9 s + 0.0 gc + 13.7 io (= 77 @ 1)]
FOO
!
←DEFN(ISPERM (U)
(IF (NLISTP U)
T
(AND (NOT (MEMB (CAR U) (CDR U)))
(ISPERM (CDR U)))))
The lemma CDR.LESSP can be used to prove that
(COUNT U) decreases according to the well-founded function
LESSP in each recursive call. Hence, ISPERM is accepted
under the definitional principle. From the definition we
can conclude that:
(OR (FALSEP (ISPERM U))
(TRUEP (ISPERM U)))
is a theorem.
[2351 cns / 7.8 s + 0.0 gc + .8 io (= 9 @ 1)]
ISPERM
!
←DEFN(LEN (X)
(IF (NLISTP X)
0
(ADD1 (LEN (CDR X)))))
The lemma CDR.LESSP can be used to show that (COUNT X)
decreases according to the well-founded function LESSP in
each recursive call. Hence, LEN is accepted under the
principle of definition. From the definition we can
conclude that (NUMBERP (LEN X)) is a theorem.
[978 cns / 4.1 s + 0.0 gc + .6 io (= 5 @ 1)]
LEN
!
←PROVE.LEMMA(FOO2 (REWRITE)
(IMPLIES (AND (NOT (LESSP (LENGTH U) N))
(ISPERM U)
(NUMBERP N)
(NOT (EQUAL N 0)))
(EQUAL (INDEX U (NTH U N)) N)))
This formula can be simplified, using the abbreviations NOT,
AND, and IMPLIES, to:
(IMPLIES (AND (NOT (LESSP (LENGTH U) N))
(ISPERM U)
(NUMBERP N)
(NOT (EQUAL N 0)))
(EQUAL (INDEX U (NTH U N)) N)),
which we will name *1.
Let us appeal to the induction principle. Five
inductions are suggested by terms in the conjecture.
However, they merge into one likely candidate induction.
We will induct according to the following scheme:
(AND (IMPLIES (NOT (NUMBERP N)) (p U N))
(IMPLIES (EQUAL N 0) (p U N))
(IMPLIES (AND (NUMBERP N)
(NOT (EQUAL N 0))
(p (CDR U) (SUB1 N)))
(p U N))).
The inequality SUB1.LESSP establishes that the measure
(COUNT N) decreases according to the well-founded function
LESSP in the induction step of the scheme. Note, however,
the inductive instance chosen for U. The above induction
scheme generates the following four new goals:
Case 4. (IMPLIES (AND (LESSP (LENGTH (CDR U)) (SUB1 N))
(NOT (LESSP (LENGTH U) N))
(ISPERM U)
(NUMBERP N)
(NOT (EQUAL N 0)))
(EQUAL (INDEX U (NTH U N)) N)).
This simplifies, applying CDR.NLISTP, and expanding the
definitions of NTH, NLISTP, ISPERM, LENGTH, EQUAL, and
LESSP, to four new conjectures:
Case 4.4.
(IMPLIES (AND (NOT (EQUAL (SUB1 N) 0))
(NOT (LISTP U))
(NOT (LESSP 0 N))
(NOT (MEMB (CAR U) (CDR U)))
(ISPERM (CDR U))
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1)))
(EQUAL (INDEX U (NTH (CDR U) (SUB1 N)))
N)).
But this again simplifies, using linear arithmetic, to:
T.
Case 4.3.
(IMPLIES
(AND (LESSP (LENGTH (CDR U)) (SUB1 N))
(LISTP U)
(NOT (LESSP (ADD1 (LENGTH (CDR U))) N))
(NOT (MEMB (CAR U) (CDR U)))
(ISPERM (CDR U))
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1)))
(EQUAL (INDEX U (NTH (CDR U) (SUB1 N)))
N)),
which we again simplify, using linear arithmetic, to:
T.
Case 4.2.
(IMPLIES (AND (NOT (EQUAL (SUB1 N) 0))
(NOT (LISTP U))
(NOT (LESSP 0 N))
(NOT (MEMB (CAR U) (CDR U)))
(ISPERM (CDR U))
(NOT (EQUAL N 0))
(EQUAL N 1))
(EQUAL (INDEX U (CAR U)) N)).
However this again simplifies, using linear arithmetic,
to:
T.
Case 4.1.
(IMPLIES
(AND (LESSP (LENGTH (CDR U)) (SUB1 N))
(LISTP U)
(NOT (LESSP (ADD1 (LENGTH (CDR U))) N))
(NOT (MEMB (CAR U) (CDR U)))
(ISPERM (CDR U))
(NOT (EQUAL N 0))
(EQUAL N 1))
(EQUAL (INDEX U (CAR U)) N)),
which we again simplify, using linear arithmetic, to:
T.
Case 3. (IMPLIES (AND (NOT (ISPERM (CDR U)))
(NOT (LESSP (LENGTH U) N))
(ISPERM U)
(NUMBERP N)
(NOT (EQUAL N 0)))
(EQUAL (INDEX U (NTH U N)) N)),
which we simplify, expanding NLISTP, INDEX, ISPERM,
LENGTH, EQUAL, and LESSP, to:
T.
Case 2. (IMPLIES (AND (EQUAL (SUB1 N) 0)
(NOT (LESSP (LENGTH U) N))
(ISPERM U)
(NUMBERP N)
(NOT (EQUAL N 0)))
(EQUAL (INDEX U (NTH U N)) N)).
Appealing to the lemma SUB1.ELIM, replace N by (ADD1 X)
to eliminate (SUB1 N). We use the type restriction lemma
noted when SUB1 was introduced to constrain the new
variable. We would thus like to prove:
(IMPLIES (AND (NUMBERP X)
(EQUAL X 0)
(NOT (LESSP (LENGTH U) (ADD1 X)))
(ISPERM U)
(NOT (EQUAL (ADD1 X) 0)))
(EQUAL (INDEX U (NTH U (ADD1 X)))
(ADD1 X))),
which we simplify, opening up the functions NUMBERP,
EQUAL, NTH, NLISTP, INDEX, ISPERM, LENGTH, and LESSP, to:
(IMPLIES (AND (NOT (LESSP (LENGTH U) 1))
(ISPERM U))
(EQUAL 1 1)).
This simplifies again, using linear arithmetic, to:
T.
Case 1. (IMPLIES
(AND (EQUAL (INDEX (CDR U) (NTH (CDR U) (SUB1 N)))
(SUB1 N))
(NOT (LESSP (LENGTH U) N))
(ISPERM U)
(NUMBERP N)
(NOT (EQUAL N 0)))
(EQUAL (INDEX U (NTH U N)) N)),
which we simplify, applying the lemma CDR.NLISTP, and
opening up the functions NTH, NLISTP, ISPERM, LENGTH,
EQUAL, LESSP, and INDEX, to four new conjectures:
Case 1.4.
(IMPLIES (AND (EQUAL 0 (SUB1 N))
(NOT (LISTP U))
(NOT (LESSP 0 N))
(NOT (MEMB (CAR U) (CDR U)))
(ISPERM (CDR U))
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1)))
(EQUAL (INDEX U (NTH (CDR U) (SUB1 N)))
N)),
which we again simplify, using linear arithmetic, to:
T.
Case 1.3.
(IMPLIES
(AND
(EQUAL (INDEX (CDR U) (NTH (CDR U) (SUB1 N)))
(SUB1 N))
(LISTP U)
(NOT (LESSP (ADD1 (LENGTH (CDR U))) N))
(NOT (MEMB (CAR U) (CDR U)))
(ISPERM (CDR U))
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1)))
(EQUAL (INDEX U (NTH (CDR U) (SUB1 N)))
N)).
But this again simplifies, applying SUB1.ADD1, and
opening up the definitions of NLISTP, INDEX, and LESSP,
to the following two new goals:
Case 1.3.2.
(IMPLIES
(AND
(EQUAL (INDEX (CDR U) (NTH (CDR U) (SUB1 N)))
(SUB1 N))
(LISTP U)
(NOT (LESSP (LENGTH (CDR U)) (SUB1 N)))
(NOT (MEMB (CAR U) (CDR U)))
(ISPERM (CDR U))
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1)))
(EQUAL (ADD1 (INDEX (CDR U)
(NTH (CDR U) (SUB1 N))))
N)),
which again simplifies, using linear arithmetic, to:
T.
Case 1.3.1.
(IMPLIES
(AND
(EQUAL (INDEX (CDR U) (NTH (CDR U) (SUB1 N)))
(SUB1 N))
(LISTP U)
(NOT (LESSP (LENGTH (CDR U)) (SUB1 N)))
(NOT (MEMB (CAR U) (CDR U)))
(ISPERM (CDR U))
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1)))
(NOT (EQUAL (CAR U)
(NTH (CDR U) (SUB1 N))))).
Appealing to the lemma CAR/CDR.ELIM, we now replace U
by (CONS Z X) to eliminate (CDR U) and (CAR U). This
produces:
(IMPLIES (AND (EQUAL (INDEX X (NTH X (SUB1 N)))
(SUB1 N))
(NOT (LESSP (LENGTH X) (SUB1 N)))
(NOT (MEMB Z X))
(ISPERM X)
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1)))
(NOT (EQUAL Z (NTH X (SUB1 N))))),
which further simplifies, clearly, to:
(IMPLIES (AND (EQUAL (INDEX X (NTH X (SUB1 N)))
(SUB1 N))
(NOT (LESSP (LENGTH X) (SUB1 N)))
(NOT (MEMB (NTH X (SUB1 N)) X))
(ISPERM X)
(NUMBERP N)
(NOT (EQUAL N 0)))
(EQUAL N 1)).
Appealing to the lemma SUB1.ELIM, replace N by
(ADD1 Z) to eliminate (SUB1 N). We rely upon the
type restriction lemma noted when SUB1 was introduced
to restrict the new variable. We thus obtain:
(IMPLIES (AND (NUMBERP Z)
(EQUAL (INDEX X (NTH X Z)) Z)
(NOT (LESSP (LENGTH X) Z))
(NOT (MEMB (NTH X Z) X))
(ISPERM X)
(NOT (EQUAL (ADD1 Z) 0)))
(EQUAL (ADD1 Z) 1)).
However this simplifies further, rewriting with
ADD1.EQUAL, and expanding the definition of NUMBERP,
to:
(IMPLIES (AND (EQUAL (INDEX X (NTH X Z)) Z)
(NOT (LESSP (LENGTH X) Z))
(NOT (MEMB (NTH X Z) X))
(ISPERM X))
(EQUAL Z 0)).
We use the above equality hypothesis by substituting
(INDEX X (NTH X Z)) for Z and throwing away the
equality. This generates the new goal:
(IMPLIES
(AND (NOT (LESSP (LENGTH X)
(INDEX X (NTH X Z))))
(NOT (MEMB (NTH X (INDEX X (NTH X Z))) X))
(ISPERM X))
(EQUAL (INDEX X (NTH X Z)) 0)).
We will try to prove the above formula by
generalizing it, replacing (NTH X Z) by Y. We would
thus like to prove:
(IMPLIES
(AND (NOT (LESSP (LENGTH X) (INDEX X Y)))
(NOT (MEMB (NTH X (INDEX X Y)) X))
(ISPERM X))
(EQUAL (INDEX X Y) 0)),
which we generalize by replacing (INDEX X Y) by A.
We restrict the new variable by recalling the type
restriction lemma noted when INDEX was introduced.
This produces:
(IMPLIES (AND (NUMBERP A)
(NOT (LESSP (LENGTH X) A))
(NOT (MEMB (NTH X A) X))
(ISPERM X))
(EQUAL A 0)).
Finally give the above formula the name *1.1.
Case 1.2.
(IMPLIES (AND (EQUAL 0 (SUB1 N))
(NOT (LISTP U))
(NOT (LESSP 0 N))
(NOT (MEMB (CAR U) (CDR U)))
(ISPERM (CDR U))
(NOT (EQUAL N 0))
(EQUAL N 1))
(EQUAL (INDEX U (CAR U)) N)).
But this simplifies again, using linear arithmetic, to:
T.
Case 1.1.
(IMPLIES
(AND
(EQUAL (INDEX (CDR U) (NTH (CDR U) (SUB1 N)))
(SUB1 N))
(LISTP U)
(NOT (LESSP (ADD1 (LENGTH (CDR U))) N))
(NOT (MEMB (CAR U) (CDR U)))
(ISPERM (CDR U))
(NOT (EQUAL N 0))
(EQUAL N 1))
(EQUAL (INDEX U (CAR U)) N)),
which we again simplify, expanding NLISTP, INDEX, and
EQUAL, to:
T.
So we now return to:
(IMPLIES (AND (NUMBERP A)
(NOT (LESSP (LENGTH X) A))
(NOT (MEMB (NTH X A) X))
(ISPERM X))
(EQUAL A 0)),
which is formula *1.1 above. Perhaps we can prove it by
induction. There are five plausible inductions. However,
they merge into one likely candidate induction. We will
induct according to the following scheme:
(AND (IMPLIES (NOT (NUMBERP A)) (p A X))
(IMPLIES (EQUAL A 0) (p A X))
(IMPLIES (AND (NUMBERP A)
(NOT (EQUAL A 0))
(p (SUB1 A) (CDR X)))
(p A X))).
The inequality SUB1.LESSP establishes that the measure
(COUNT A) decreases according to the well-founded function
LESSP in the induction step of the scheme. Note, however,
the inductive instance chosen for X. The above induction
scheme leads to four new goals:
Case 4. (IMPLIES (AND (LESSP (LENGTH (CDR X)) (SUB1 A))
(NUMBERP A)
(NOT (LESSP (LENGTH X) A))
(NOT (MEMB (NTH X A) X))
(ISPERM X))
(EQUAL A 0)).
This simplifies, appealing to the lemmas CDR.NLISTP and
CAR.NLISTP, and opening up the definitions of NLISTP,
ISPERM, NTH, MEMB, LENGTH, EQUAL, and LESSP, to four new
formulas:
Case 4.4.
(IMPLIES
(AND (NOT (EQUAL (SUB1 A) 0))
(NUMBERP A)
(NOT (LISTP X))
(NOT (LESSP 0 A))
(NOT (EQUAL A 1))
(NOT (MEMB (NTH (CDR X) (SUB1 A)) X))
(NOT (MEMB (CAR X) (CDR X)))
(ISPERM (CDR X)))
(EQUAL A 0)).
This again simplifies, using linear arithmetic, to:
T.
Case 4.3.
(IMPLIES
(AND (LESSP (LENGTH (CDR X)) (SUB1 A))
(NUMBERP A)
(LISTP X)
(NOT (LESSP (ADD1 (LENGTH (CDR X))) A))
(NOT (EQUAL A 1))
(NOT (MEMB (NTH (CDR X) (SUB1 A)) X))
(NOT (MEMB (CAR X) (CDR X)))
(ISPERM (CDR X)))
(EQUAL A 0)).
This again simplifies, using linear arithmetic, to:
T.
Case 4.2.
(IMPLIES (AND (NOT (EQUAL (SUB1 A) 0))
(NOT (LISTP X))
(NOT (LESSP 0 A))
(EQUAL A 1)
(NOT (MEMB (CAR X) X))
(NOT (MEMB (CAR X) (CDR X)))
(ISPERM (CDR X)))
(EQUAL A 0)),
which we again simplify, using linear arithmetic, to:
T.
Case 4.1.
(IMPLIES
(AND (LESSP (LENGTH (CDR X)) (SUB1 A))
(LISTP X)
(NOT (LESSP (ADD1 (LENGTH (CDR X))) A))
(EQUAL A 1)
(NOT (MEMB (CAR X) X))
(NOT (MEMB (CAR X) (CDR X)))
(ISPERM (CDR X)))
(EQUAL A 0)),
which we again simplify, using linear arithmetic, to:
T.
Case 3. (IMPLIES (AND (MEMB (NTH (CDR X) (SUB1 A)) (CDR X))
(NUMBERP A)
(NOT (LESSP (LENGTH X) A))
(NOT (MEMB (NTH X A) X))
(ISPERM X))
(EQUAL A 0)),
which simplifies, applying CDR.NLISTP and CAR.NLISTP, and
opening up NLISTP, ISPERM, NTH, MEMB, LENGTH, EQUAL, and
LESSP, to two new goals:
Case 3.2.
(IMPLIES
(AND (MEMB (NTH (CDR X) (SUB1 A)) (CDR X))
(NUMBERP A)
(LISTP X)
(NOT (LESSP (ADD1 (LENGTH (CDR X))) A))
(NOT (EQUAL A 1))
(NOT (MEMB (NTH (CDR X) (SUB1 A)) X))
(NOT (MEMB (CAR X) (CDR X)))
(ISPERM (CDR X)))
(EQUAL A 0)).
But this simplifies again, unfolding NLISTP and MEMB,
to:
T.
Case 3.1.
(IMPLIES
(AND (MEMB (NTH (CDR X) (SUB1 A)) (CDR X))
(LISTP X)
(NOT (LESSP (ADD1 (LENGTH (CDR X))) A))
(EQUAL A 1)
(NOT (MEMB (CAR X) X))
(NOT (MEMB (CAR X) (CDR X)))
(ISPERM (CDR X)))
(EQUAL A 0)),
which we again simplify, opening up EQUAL, NLISTP, and
MEMB, to:
T.
Case 2. (IMPLIES (AND (NOT (ISPERM (CDR X)))
(NUMBERP A)
(NOT (LESSP (LENGTH X) A))
(NOT (MEMB (NTH X A) X))
(ISPERM X))
(EQUAL A 0)),
which simplifies, rewriting with CDR.NLISTP and
CAR.NLISTP, and opening up the functions NLISTP, ISPERM,
NTH, MEMB, LENGTH, EQUAL, and LESSP, to:
T.
Case 1. (IMPLIES (AND (EQUAL (SUB1 A) 0)
(NUMBERP A)
(NOT (LESSP (LENGTH X) A))
(NOT (MEMB (NTH X A) X))
(ISPERM X))
(EQUAL A 0)).
Applying the lemma SUB1.ELIM, replace A by (ADD1 Z) to
eliminate (SUB1 A). We rely upon the type restriction
lemma noted when SUB1 was introduced to restrict the new
variable. This generates:
(IMPLIES (AND (NUMBERP Z)
(EQUAL Z 0)
(NOT (LESSP (LENGTH X) (ADD1 Z)))
(NOT (MEMB (NTH X (ADD1 Z)) X))
(ISPERM X))
(EQUAL (ADD1 Z) 0)),
which we simplify, unfolding the definitions of EQUAL,
NUMBERP, NTH, NLISTP, MEMB, LENGTH, and LESSP, to:
T.
That finishes the proof of *1.1, which, consequently,
finishes the proof of *1. Q.E.D.
[41960 cns / 228.3 s + 23.9 gc + 27.6 io (= 285 @ 1)]
FOO2
!
←DEFN(INVERT2 (U N M)
(IF (ZEROP N)
NIL
(CONS (INDEX U (ADD1 (DIFFERENCE M N)))
(INVERT2 U (SUB1 N) M))))
The lemma SUB1.LESSP establishes that (COUNT N) goes
down according to the well-founded function LESSP in each
recursive call. Hence, INVERT2 is accepted under the
definitional principle. Observe that:
(OR (LITATOM (INVERT2 U N M))
(LISTP (INVERT2 U N M)))
is a theorem.
[1779 cns / 6.8 s + 0.0 gc + .6 io (= 8 @ 1)]
INVERT2
!
←DEFN(INVERT (U)
(INVERT2 U (LENGTH U) (LENGTH U)))
Note that (OR (LITATOM (INVERT U)) (LISTP (INVERT U)))
is a theorem.
[568 cns / 2.6 s + 0.0 gc + .3 io (= 3 @ 1)]
INVERT
-------
Here's a report on my efforts at proving your theorem about
inverting permutations.
The theorem-prover proved a version of the theorem you wanted:
Theorem. MAIN:
(IMPLIES (AND (PLISTP U)
(HAS.ALL.NUMS U (LENGTH U))
(ISPERM U)
(BOUNDED U (LENGTH U)))
(EQUAL (INVERT (INVERT U)) U))
Let me describe the hypotheses.
PLISTP checks that its argument ends in a NIL. That's
necessary to maintain strict equality. (The definitions
and theorems are included at the end of this message.)
HAS.ALL.NUMS checks that its first argument contains as members
all of the numbers from 1 up to the second argument.
(HAS.ALL.NUMS U (LENGTH U)) is a necessary and sufficient
condition for U to be a number permuation as you described it.
ISPERM is your function that checks for the absence of duplications.
BOUNDED checks that every member of the first argument is
a nonzero number less than or equal to the second argument.
The last two hypotheses are logically implied by the HAS.ALL.NUMS
hypothesis, but I couldn't see a quick way to prove it, so
I used all the hypotheses.
To prove MAIN, I took the route of using as lemmas the two lemmas
you mentioned that we did not try proving when you were here:
nth(invert(u),n) = index(u,n)
index(invert(u),n) = nth(u,n)
The somewhat more general formulation of the first lemma is:
Theorem. NTH.INVERT:
(IMPLIES
(AND (NOT (ZEROP N))
(NOT (LESSP I N)))
(EQUAL (NTH (INVERT2 U I J) N)
(INDEX U
(ADD1 (DIFFERENCE J
(DIFFERENCE I (SUB1 N)))))))
The version of the second lemma I proved follows. I
called it "weak" because I put in an extra hypothesis (the
first) that was relieved later.
Theorem. MAIN.WEAK:
(IMPLIES (AND (ISPERM (INVERT2 U (LENGTH U) (LENGTH U)))
(NOT (LESSP (LENGTH U) N))
(NUMBERP N)
(NOT (EQUAL N 0))
(ISPERM U)
(BOUNDED U (LENGTH U)))
(EQUAL (INDEX (INVERT2 U (LENGTH U) (LENGTH U))
N)
(NTH U N)))
The proof of this lemma was extremely tricky for the
theorem-prover. It is more accurate to say that the
theorem-prover was "tricked" into proving it by first
proving FOO2.BRIDGE, suggested by J, (below). It is true
that
index(inv(u),n) = nth(u,n)
is a logical consequence of
index(u,nth(u,n)) = n and
nth(invert(u),n) = index(u,n)
but the only proofs I know involve a nasty phenonemenon handled
well in the theorem-prover of Knuth and Bendix but not in ours.
One cute trick was used to derive invert(invert(u)) = u from
nth(invert(invert(u)),n) = nth(u,n). The theorem FIRST.DIFF.EQUAL
states that u = v if and only if (nth(u,j) /= nth(v,j) where j
is the first place that u and v differ, as calculated by
the function FIRST.DIFF.)
I'll be happy to send you the full proof-printout if you
want, or you can FTP it from [SRI-VIS11]<BOYER>JMC.PROOFS.
(SRI-VIS11 is the current name of our first F2.) If you'd
like to come visit to talk about the proofs (or anything
else), I'd be pleased.
In conclusion, here is the list of definitions and theorems that
I had to ask the theorem-prover to prove to get MAIN.
Definition.
(NTH U N)
=
(IF (ZEROP N)
U
(IF (EQUAL N 1)
(CAR U)
(NTH (CDR U) (SUB1 N))))
Definition.
(INDEX U X)
=
(IF (NLISTP U)
0
(IF (EQUAL (CAR U) X)
1
(ADD1 (INDEX (CDR U) X))))
Definition.
(MEMB X Y)
=
(IF (NLISTP Y)
(FALSE)
(IF (EQUAL X (CAR Y))
T
(MEMB X (CDR Y))))
Theorem. FOO:
(IMPLIES (MEMB X U)
(EQUAL (NTH U (INDEX U X)) X))
Definition.
(ISPERM U)
=
(IF (NLISTP U)
T
(AND (NOT (MEMB (CAR U) (CDR U)))
(ISPERM (CDR U))))
Theorem. FOO2:
(IMPLIES (AND (NOT (LESSP (LENGTH U) N))
(ISPERM U)
(NUMBERP N)
(NOT (EQUAL N 0)))
(EQUAL (INDEX U (NTH U N)) N))
Definition.
(INVERT2 U N M)
=
(IF (ZEROP N)
NIL
(CONS (INDEX U (ADD1 (DIFFERENCE M N)))
(INVERT2 U (SUB1 N) M)))
Definition.
(INVERT U)
=
(INVERT2 U (LENGTH U) (LENGTH U))
Theorem. NTH.INVERT:
(IMPLIES
(AND (NOT (ZEROP N))
(NOT (LESSP I N)))
(EQUAL (NTH (INVERT2 U I J) N)
(INDEX U
(ADD1 (DIFFERENCE J
(DIFFERENCE I (SUB1 N)))))))
Theorem. DIFF.DIFF:
(IMPLIES (AND (NUMBERP X) (NOT (LESSP I X)))
(EQUAL (DIFFERENCE I (DIFFERENCE I X))
X))
Theorem. NTH.INVERT.MAIN:
(IMPLIES (AND (NOT (ZEROP N))
(NOT (LESSP (LENGTH U) N)))
(EQUAL (NTH (INVERT2 U (LENGTH U) (LENGTH U))
N)
(INDEX U N)))
Theorem. FOO2.BRIDGE:
(IMPLIES (AND (EQUAL A (NTH U N))
(NOT (LESSP (LENGTH U) N))
(ISPERM U)
(NUMBERP N)
(NOT (EQUAL N 0)))
(EQUAL (EQUAL (INDEX U A) N) T))
Definition.
(BOUNDED L N)
=
(IF (NLISTP L)
T
(AND (NOT (ZEROP (CAR L)))
(NOT (LESSP N (CAR L)))
(BOUNDED (CDR L) N)))
Theorem. LENGTH.INVERT:
(IMPLIES (NUMBERP I)
(EQUAL (LENGTH (INVERT2 U I J)) I))
Definition.
(HAS.ALL.NUMS L N)
=
(IF (ZEROP N)
T
(AND (MEMB N L)
(HAS.ALL.NUMS L (SUB1 N))))
Theorem. BOUNDED.IS.A.QUANTIFIER:
(IMPLIES (AND (BOUNDED L N)
(NOT (LESSP (LENGTH L) I))
(NUMBERP I)
(NOT (EQUAL I 0)))
(AND (NOT (LESSP N (NTH L I)))
(NOT (EQUAL (NTH L I) 0))
(NUMBERP (NTH L I))))
Theorem. MAIN.WEAK:
(IMPLIES (AND (ISPERM (INVERT2 U (LENGTH U) (LENGTH U)))
(NOT (LESSP (LENGTH U) N))
(NUMBERP N)
(NOT (EQUAL N 0))
(ISPERM U)
(BOUNDED U (LENGTH U)))
(EQUAL (INDEX (INVERT2 U (LENGTH U) (LENGTH U))
N)
(NTH U N)))
Theorem. INDEX.0:
(EQUAL (EQUAL (INDEX U A) 0)
(NLISTP U))
Theorem. INDEX.EQUAL:
(IMPLIES (AND (MEMB A U)
(MEMB B U)
(NOT (EQUAL A B)))
(NOT (EQUAL (INDEX U A) (INDEX U B))))
Theorem. HAS.ALL.NUMS.IS.A.QUANTIFIER:
(IMPLIES (AND (HAS.ALL.NUMS L N)
(LESSP I (ADD1 N))
(NUMBERP I)
(NOT (EQUAL I 0)))
(MEMB I L))
Theorem. DIFFERENCE.LESSP:
(IMPLIES (NOT (LESSP I J))
(EQUAL (DIFFERENCE J I) 0))
Theorem. MEMB.INVERT2:
(IMPLIES (AND (HAS.ALL.NUMS U (LENGTH U))
(LESSP I (ADD1 (LENGTH U)))
(NUMBERP I)
(NOT (EQUAL I 0))
(LESSP I
(ADD1 (DIFFERENCE (LENGTH U) P)))
(NOT (LESSP (LENGTH U) P)))
(NOT (MEMB (INDEX U I)
(INVERT2 U P (LENGTH U)))))
Theorem. ISPERM.INVERT2.1:
(IMPLIES (AND (HAS.ALL.NUMS U (LENGTH U))
(NOT (LESSP (LENGTH U) I)))
(ISPERM (INVERT2 U I (LENGTH U))))
Definition.
(PLISTP L)
=
(IF (NLISTP L)
(EQUAL L NIL)
(PLISTP (CDR L)))
Definition.
(FIRST.DIFF L1 L2)
=
(IF (NLISTP L1)
0
(IF (NOT (EQUAL (CAR L1) (CAR L2)))
1
(ADD1 (FIRST.DIFF (CDR L1) (CDR L2)))))
Theorem. LENGTH.0:
(IMPLIES (PLISTP L)
(EQUAL (EQUAL (LENGTH L) 0)
(EQUAL L NIL)))
Theorem. PLISTP.INVERT2:
(PLISTP (INVERT2 U I J))
Theorem. FIRST.DIFF.LENGTH:
(NOT (LESSP (LENGTH L1)
(FIRST.DIFF L1 L2)))
Theorem. NTH.INVERT.MAIN1:
(IMPLIES (AND (EQUAL A (LENGTH U))
(EQUAL B (LENGTH U))
(NOT (ZEROP N))
(NOT (LESSP (LENGTH U) N)))
(EQUAL (NTH (INVERT2 U A B) N)
(INDEX U N)))
Theorem. FIRST.DIFF.EQUAL:
(IMPLIES (AND (PLISTP L1)
(PLISTP L2)
(EQUAL (LENGTH L1) (LENGTH L2)))
(EQUAL (EQUAL L1 L2)
(EQUAL (NTH L1
(IF (ZEROP (FIRST.DIFF L1 L2))
1
(FIRST.DIFF L1 L2)))
(NTH L2
(IF (ZEROP (FIRST.DIFF L1 L2))
1
(FIRST.DIFF L1 L2))))))
Theorem. MAIN:
(IMPLIES (AND (PLISTP U)
(HAS.ALL.NUMS U (LENGTH U))
(ISPERM U)
(BOUNDED U (LENGTH U)))
(EQUAL (INVERT (INVERT U)) U))
-------
-------
PROOFS[F80,JMC] contains the material I received from Boyer, but the
messages were addressed to you also.